(module substitutions  (lib "eopl.ss" "eopl")
  ;; (require "drscheme-init.scm")
  (require "lang.scm")

  (provide substitution? empty-subst extend-subst apply-subst)

;;;;;;;;;;;;;;;; Unit substitution ;;;;;;;;;;;;;;;;

  ;; apply-one-subst: type * var * type -> type
  ;; (apply-one-subst oldty var newty) returns the type obtained by
  ;; substituting newty for every occurrence of var in oldty. 

  (define apply-one-subst
    (lambda (oldty var newty)
      (cases type oldty
        (proc-type (arg-type result-type)
          (proc-type
            (apply-one-subst arg-type var newty)
            (apply-one-subst result-type var newty)))
        (tvar-type (sn)
          (if (equal? oldty var) newty oldty))
        ;; named-types are constants
        ;; (named-type (name) oldty)
        (else oldty))))

;;;;;;;;;;;;;;;; Substitutions ;;;;;;;;;;;;;;;;

  ;; a substitution is a map from unknown types to types.
  ;; we'll represent this as an association list.

  (define pair-of
    (lambda (pred1 pred2)
      (lambda (val)
        (and (pair? val) (pred1 (car val)) (pred2 (cdr val))))))

  (define substitution? 
    (list-of (pair-of tvar-type? type?)))

  ;; basic observer: apply-subst
  ;; apply-subst : subst * type -> type

  (define apply-subst
    (lambda (subst ty)
      (cases type ty
        (named-type (name) ty)
        (int-type () (int-type))
        (bool-type () (bool-type))
        (proc-type (t1 t2)
          (proc-type
            (apply-subst subst t1)
            (apply-subst subst t2)))
        (tvar-type (sn)
          (let ((tmp (assoc ty subst)))
            (if tmp
              (cdr tmp)
              ty)))
        (qualified-type (m-name t-name) ty)
        )))

  ;; empty-subst : () -> subst
  ;; produces a representation of the empty substitution.

  (define empty-subst (lambda () '()))

  ;; extend-subst : tvar-type * type * subst -> subst

  ;; (extend-subst v t s) produces a substitution with the property
  ;; that for all t0,
  
  ;;   (apply-subst (extend-subst v t s) t0)
  ;;   = (apply-one-subst v t (apply-subst s t0))

  ;; this means that for any type variable v' in the domain of s,

  ;;   (apply-subst (extend-subst v t s) v')
  ;;   = (apply-one-subst v t (apply-subst s v'))

  ;; so we extend the substitution with a new element, and apply [t/v] to every
  ;; element already in the substitution. 

  (define extend-subst
    (lambda (v t subst)
      (cons
        (cons v t)
        (map 
          (lambda (p)
            (let ((oldvar (car p))
                  (oldval (cdr p)))
              (cons
                oldvar
                (apply-one-subst oldval v t))))
          subst))))

  )



